COMMENT ⊗   VALID 00006 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	first application: the case of alists
C00003 00003	first application: to alists. Lemma:inj implies disjoint 
C00006 00004	the sets in the sequence have positive multiplicity
C00009 00005	lemma mult_mult
C00011 00006	the main result for permutp: theorem permutp_injectp
C00016 ENDMK
C⊗;
;first application: the case of alists
(wipe-out)
(get-proofs pigeon prf ekl sys)
(proof alpig)

(axiom |∀u.inj(u)⊃disjoint(λm.mkset(nth(u,m)),length u)|)
(label inj_disj)
  
(axiom |∀u v.mklset u=mklset v⊃
             (∀m.m<length u⊃1≤mult(v,mkset nth(u,m)))|)
(label permutp_injectp_lemma)

(axiom |∀u v.mklset u = mklset v ∧
             (∀k.k<length u⊃mult(v,mkset nth(u,k))=1)⊃
             (∀i.i<length v⊃mult(v,mkset nth(v,i))=1)|)
(label mult_mult)

(axiom |∀alist.permutp(alist)⊃injectp(alist)|)
(label theorem_permutp_injectp)
(save-proofs alpig)
;first application: to alists. Lemma:inj implies disjoint 
(wipe-out)
(get-proofs pigeon prf ekl sys)
    (proof inj_disj)

;a main lemma for the induction step

1.  (assume |inj u|)
    (label injdsj0)

2.  (rw * (open inj))
    (label injdsj1)
    ;∀N M.N<LENGTH U∧M<LENGTH U∧NTH(U,N)=NTH(U,M)⊃N=M

3.  (assume |n<length u|)
    (label injdsj2)

4.  (assume |(un(λm.mkset(nth(u,m)),n))(xv)∧(mkset(nth(u,n)))(xv)|)
    (label injdsj3)

;need mksetfact

5.  (ue ((u.u)(n.n)) mksetfact (open lesseq) injdsj2)
    ;UN(λM.MKSET(NTH(U,M)),N)=(λX.(∃K.K<N∧NTH(U,K)=X))

6.  (rw injdsj3 (use * mode: exact) (open mkset) injdsj2)
    ;(∃K.K<N∧NTH(U,K)=XV)∧XV=NTH(U,N)
    (label injdsj4)

7.  (define kv |kv<n∧nth(u,kv)=xv| (use *))
    (label injdsj5)

8.  (derive |kv<length u∧nth(u,kv)=nth(u,n)| (* injdsj2 transitivity_of_order)
       (use injdsj4 mode: always direction: reverse))

9.  (derive |kv=n| (injdsj2 * injdsj1))

10. (rw injdsj5 (use * mode: exact) irreflexivity_of_order)
    ;FALSE
    ;deps: (INJDSJ0 INJDSJ3 INJDSJ2)

11. (ci injdsj3)
    ;¬((UN(λM.MKSET(NTH(U,M)),N))(XV)∧(MKSET(NTH(U,N)))(XV))

12. (ci (injdsj0 injdsj2))
    ;INJ(U)∧N<LENGTH U⊃¬((UN(λM.MKSET(NTH(U,M)),N))(XV)∧(MKSET(NTH(U,N)))(XV))
    (label injdsj_lemma)

;the theorem follows

13. (ue (a |λn.inj(u)∧n≤length(u)⊃disjoint(λm.mkset nth(u,m),n)|) proof_by_induction
       (open disjoint disj_pair intersection emptyp) 
        (use less_lesseqsucc mode: always direction: reverse)
        (use injdsj_lemma mode: always)(part 1#2#1#1 (open lesseq)))
    ;∀N.INJ(U)∧N≤LENGTH U⊃DISJOINT(λM.MKSET(NTH(U,M)),N)

14. (ue (n |length u|) * (open lesseq))
    ;INJ(U)⊃DISJOINT(λM.MKSET(NTH(U,M)),LENGTH U)
;the sets in the sequence have positive multiplicity
    (proof permutp_injectp_lemma)

1.  (assume |mklset u=mklset v|)
    (label pil1)

2.  (assume |n<length u|)
    (label pil2)

;use nthmember

3.  (trw |nth(u,n)ε mklset u| (open epsilon mklset) 
         nthmember pil2)
    ;NTH(U,N)εMKLSET(U)
    ;deps: (PIL2)

;now use line pil1

4.  (rw * (use pil1 mode: exact))
    ;NTH(U,N)εMKLSET(V)
    ;deps: (PIL1 PIL2)

;Finally, using MKLSET-FACT, we prove the existence of a kv such that 
;nth(v,kv)=nth(u,n)

;labels: MKLSET_FACT 
;(AXIOM |∀U.MKLSET(U)=(λX.(∃K.K<LENGTH U∧NTH(U,K)=X))|)

5.  (rw * (use mklset_fact mode: exact) (open epsilon mkset))
    ;∃K.K<LENGTH V∧NTH(V,K)=NTH(U,N)
    ;deps: (PIL1 PIL2)

6.  (define kv |kv<length(v)∧nth(v,kv)=nth(u,n)| *)
    (label pil3)
    ;deps: (PIL1 PIL2)

7.  (trw |member(nth(v,kv),v)| nthmember pil3)
    ;MEMBER(NTH(V,KV),V)
    (label pil4)

;Therefore the set mkset(nth(u,n)) has positive multiplicity in v.

;labels: MEMBER_MULT 
;(AXIOM |∀U Y A.MEMBER(Y,U)∧A(Y)⊃1≤MULT(U,A)|)

8.  (ue ((u.v)(y.|nth(v,kv)|)(a.|mkset nth(u,n)|)) member_mult 
        (part 1(open mkset)) pil2 pil4 (use pil3 mode: always))
    ;1≤MULT(V,MKSET(NTH(U,N)))
    ;deps: (PIL1 PIL2)

9.  (ci (pil1 pil2))
    ;MKLSET(U)=MKLSET(V)∧N<LENGTH U⊃1≤MULT(V,MKSET(NTH(U,N)))

;cosmetics

10. (derive |∀u v.mklset u=mklset v⊃(∀m.m<length u⊃1≤mult(v,mkset nth(u,m)))| *)
;lemma mult_mult
    (proof mult_mult)

1.  (assume |mklset u = mklset v|)
    (label mm1)

2.  (assume |∀m.m<length u ⊃ mult(v,mkset nth(u,m))=1|)
    (label mm2)

3.  (assume |i<length v|)
    (label mm3)

4.  (trw |nth(v,i) ε mklset v| (open epsilon mklset)
         (use * nthmember mode: exact) )
    ;NTH(V,I)εMKLSET(V)

5.  (rw * (use mm1 mode: exact direction: reverse))
    ;NTH(V,I)εMKLSET(U)

6.  (rw * (use mklset_fact mode: exact) (open epsilon))
    ;∃K.K<LENGTH U∧NTH(U,K)=NTH(V,I)

7.  (define mv |mv<length u ∧nth(u,mv)=nth(v,i)| *)
    (label mm4)
    ;MV is unknown.
    ;the symbol MV is given the same declaration as M
    ;deps: (MM1 MM3)

8.  (ue (m mv) mm2 (use * mode: always))
    ;MULT(V,MKSET(NTH(V,I)))=1
    ;deps: (MM1 MM2 MM3)

9.  (ci mm3)
    ;I<LENGTH V⊃MULT(V,MKSET(NTH(V,I)))=1
    ;deps: (MM1 MM2)

10. (ci (mm1 mm2))
    ;MKLSET(U)=MKLSET(V)∧(∀M.M<LENGTH U⊃MULT(V,MKSET(NTH(U,M)))=1)⊃
    ;(I<LENGTH V⊃MULT(V,MKSET(NTH(V,I)))=1)
;the main result for permutp: theorem permutp_injectp

    (proof permutp_injectp)

1.  (assume |permutp alist|)
    (label permutp_injectp1)

2.  (rw * (open permutp))
    ;FUNCTP(ALIST)∧MKLSET(DOM(ALIST))=MKLSET(RANGE(ALIST))
    (label permutp_injectp2)

3.  (rw * (open functp))
    ;UNIQUENESS(DOM(ALIST))∧MKLSET(DOM(ALIST))=MKLSET(RANGE(ALIST))
    (label permutp_injectp3)

      
;first step: disjointness of a suitable sequence of sets


;labels: UNIQUENESS_INJECTIVITY 
;(AXIOM |∀U.UNIQUENESS(U)≡INJ(U)|)

;labels: INJ_DISJ 
;(AXIOM |∀U.INJ(U)⊃DISJOINT(λM.MKSET(NTH(U,M)),LENGTH U)|)

4.  (derive |inj(dom(alist))| (* uniqueness_injectivity))
    ;deps: (PERMUTP_INJECTP1)

5.  (derive |disjoint(λm.mkset(nth(dom(alist),m)),length (dom(alist)))|
          (* inj_disj))
    (label permutp_injectp4)


;second step: multiplicity of the sets in the sequence is positive


;labels: PERMUTP_INJECTP_LEMMA 
;(AXIOM
;  |∀U V.MKLSET(U)=MKLSET(V)⊃(∀M.M<LENGTH U⊃1≤MULT(V,MKSET(NTH(U,M))))|)

6.  (ue ((u.|dom alist|)(v.|range alist|)) permutp_injectp_lemma
        (permutp_injectp3 permutp_injectp4))
    ;∀M.M<LENGTH (DOM(ALIST))⊃1≤MULT(RANGE(ALIST),MKSET(NTH(DOM(ALIST),M)))
    (label permutp_injectp5)


;third step: application of the pigeon hole principle


;labels: PIGEONLIST 
;  (AXIOM
;    |∀SETSEQ U.DISJOINT(SETSEQ,LENGTH U)∧(∀K.K<LENGTH U⊃1≤MULT(U,SETSEQ(K)))⊃
;               (∀K.K<LENGTH U⊃1=MULT(U,SETSEQ(K)))|)

;need also
;labels: DOMRANGELENGTH 
;(AXIOM |∀ALIST.LENGTH (DOM(ALIST))=LENGTH (RANGE(ALIST))|)

7.  (ue ((setseq.|λm.mkset nth(dom alist,m)|)(u.|range alist|)) pigeonlist
        (use domrangelength mode: exact direction: reverse)
        permutp_injectp4 permutp_injectp5)
    ;∀K.K<LENGTH (DOM(ALIST))⊃1=MULT(RANGE(ALIST),MKSET(NTH(DOM(ALIST),K)))


;fourth step: injectivity


;labels: MULT_MULT 
;∀U V.MKLSET(U)=MKLSET(V)∧(∀K.K<LENGTH U⊃MULT(V,MKSET(NTH(U,K)))=1)⊃
;     (∀I.I<LENGTH V⊃MULT(V,MKSET(NTH(V,I)))=1)

8.  (ue ((u.|dom(alist)|)(v.|range(alist)|)) mult_mult
        permutp_injectp3 *)
    ;∀I.I<LENGTH (RANGE(ALIST))⊃MULT(RANGE(ALIST),MKSET(NTH(RANGE(ALIST),I)))=1
    ;deps: (PERMUTP_INJECTP1)

;apply mult_inj

;labels: MULT_INJ 
;∀V.(∀K.K<LENGTH V⊃MULT(V,MKSET(NTH(V,K)))=1)⊃INJ(V)

9.  (ue (v |range alist|) mult_inj *)
    ;INJ(RANGE(ALIST))
    ;deps: (PERMUTP_INJECTP1)

10. (derive |uniqueness(range alist)| (* uniqueness_injectivity))
    ;deps: (PERMUTP_INJECTP1)

11. (derive |injectp alist| (permutp_injectp2 *)(open injectp))
    ;deps: (PERMUTP_INJECTP1)

12. (ci (permutp_injectp1))
    ;PERMUTP(ALIST)⊃INJECTP(ALIST)